Definitions | t T, #$n, x:A. B(x), A B, a < b, void, x:A B(x), P  Q, False, A, {x:A| B(x)} , , , <a, b>, b,  b, , s = t, prop{i:l}, x:A B(x), inc-snd(p), loc(e), es-vartype(es; i; x), P Q, es-dtype(es; i; x; T), es-after(es; x; e), Type, inc-fst(p), eq_id(a; b), left + right, P   Q, Unit,  x. t(x), let x = a in b(x), if b then t else f fi , EqDecider(T), event_system{i:l}, let x,y = A in B(x;y), t.1, es-E(es), atom{$n:n}, case b of inl(x) => s(x) | inr(y) => t(y), A c B, f(a), f-rank{i:l}(x; free; es; e), x.A(x), x changed before e, True, T, es-locl(es; e; e'), x:A. B(x), SWellFounded(R(x;y)), ge(i; j), -n, n + m, n - m, id-deq, Id, (last change to x before e) |